1: | active(from(X)) | → mark(cons(X,from(s(X)))) | |
2: | active(length(nil)) | → mark(0) | |
3: | active(length(cons(X,Y))) | → mark(s(length1(Y))) | |
4: | active(length1(X)) | → mark(length(X)) | |
5: | active(from(X)) | → from(active(X)) | |
6: | active(cons(X1,X2)) | → cons(active(X1),X2) | |
7: | active(s(X)) | → s(active(X)) | |
8: | from(mark(X)) | → mark(from(X)) | |
9: | cons(mark(X1),X2) | → mark(cons(X1,X2)) | |
10: | s(mark(X)) | → mark(s(X)) | |
11: | proper(from(X)) | → from(proper(X)) | |
12: | proper(cons(X1,X2)) | → cons(proper(X1),proper(X2)) | |
13: | proper(s(X)) | → s(proper(X)) | |
14: | proper(length(X)) | → length(proper(X)) | |
15: | proper(nil) | → ok(nil) | |
16: | proper(0) | → ok(0) | |
17: | proper(length1(X)) | → length1(proper(X)) | |
18: | from(ok(X)) | → ok(from(X)) | |
19: | cons(ok(X1),ok(X2)) | → ok(cons(X1,X2)) | |
20: | s(ok(X)) | → ok(s(X)) | |
21: | length(ok(X)) | → ok(length(X)) | |
22: | length1(ok(X)) | → ok(length1(X)) | |
23: | top(mark(X)) | → top(proper(X)) | |
24: | top(ok(X)) | → top(active(X)) | |
25: | ACTIVE(from(X)) | → CONS(X,from(s(X))) | |
26: | ACTIVE(from(X)) | → FROM(s(X)) | |
27: | ACTIVE(from(X)) | → S(X) | |
28: | ACTIVE(length(cons(X,Y))) | → S(length1(Y)) | |
29: | ACTIVE(length(cons(X,Y))) | → LENGTH1(Y) | |
30: | ACTIVE(length1(X)) | → LENGTH(X) | |
31: | ACTIVE(from(X)) | → FROM(active(X)) | |
32: | ACTIVE(from(X)) | → ACTIVE(X) | |
33: | ACTIVE(cons(X1,X2)) | → CONS(active(X1),X2) | |
34: | ACTIVE(cons(X1,X2)) | → ACTIVE(X1) | |
35: | ACTIVE(s(X)) | → S(active(X)) | |
36: | ACTIVE(s(X)) | → ACTIVE(X) | |
37: | FROM(mark(X)) | → FROM(X) | |
38: | CONS(mark(X1),X2) | → CONS(X1,X2) | |
39: | S(mark(X)) | → S(X) | |
40: | PROPER(from(X)) | → FROM(proper(X)) | |
41: | PROPER(from(X)) | → PROPER(X) | |
42: | PROPER(cons(X1,X2)) | → CONS(proper(X1),proper(X2)) | |
43: | PROPER(cons(X1,X2)) | → PROPER(X1) | |
44: | PROPER(cons(X1,X2)) | → PROPER(X2) | |
45: | PROPER(s(X)) | → S(proper(X)) | |
46: | PROPER(s(X)) | → PROPER(X) | |
47: | PROPER(length(X)) | → LENGTH(proper(X)) | |
48: | PROPER(length(X)) | → PROPER(X) | |
49: | PROPER(length1(X)) | → LENGTH1(proper(X)) | |
50: | PROPER(length1(X)) | → PROPER(X) | |
51: | FROM(ok(X)) | → FROM(X) | |
52: | CONS(ok(X1),ok(X2)) | → CONS(X1,X2) | |
53: | S(ok(X)) | → S(X) | |
54: | LENGTH(ok(X)) | → LENGTH(X) | |
55: | LENGTH1(ok(X)) | → LENGTH1(X) | |
56: | TOP(mark(X)) | → TOP(proper(X)) | |
57: | TOP(mark(X)) | → PROPER(X) | |
58: | TOP(ok(X)) | → TOP(active(X)) | |
59: | TOP(ok(X)) | → ACTIVE(X) | |